(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(declare-fun v1 () (_ BitVec 4))
(declare-fun v2 () (_ BitVec 4))
(declare-fun v3 () (_ BitVec 4))
(declare-fun v4 () (_ BitVec 4))
(assert (= ((_ extract 2 0) v1) ((_ extract 3 1) v1)))
(assert (not (= ((_ extract 0 0) v1) ((_ extract 3 3) v1))))
(check-sat)
(exit)
